package karpiel.boguchwal.wojciech.przemek

import karpiel.boguchwal.wojciech.przemek.Ast._

class CommonParsingCases(parse: String => Ast) {
  def readMeCases(): Map[Ast, Ast] = {
    //readme
    Map(
      parse("(lambda (A (Universe 0)) (lambda (x A) x))") -> PiValue(NamedType("A", Universe(0)), PiValue(NamedType("x", Var("A")), Var("x"))),
      parse("((lambda (A (Universe 0)) (lambda (x A) x)) Unit)") -> PiElim(PiValue(NamedType("A", Universe(0)), PiValue(NamedType("x", Var("A")), Var("x"))), UnitType),
      parse("(((lambda (A (Universe 0)) (lambda (x A) x)) Unit) tt)") ->
        PiElim(PiElim(PiValue(NamedType("A", Universe(0)), PiValue(NamedType("x", Var("A")), Var("x"))), UnitType), UnitValue)
    )
  }


  def nat(): Map[Ast, Ast] = {
    //Nat
    Map(
      Bruinizer.bruinize(parse("(W (lambda (b Bool) ((Bool-ind Unit Empty) b)))"))(Context.Empty, RealCache()) -> StdLib.Nat.natType,

      Bruinizer.bruinize(parse(
        "((lambda (Nat (Universe 0))\n   (WSup Nat false (lambda (e Empty) ((Empty-ind Nat) e))))\n (W (lambda (b Bool) ((Bool-ind Unit Empty) b))))"
      ))(Context.Empty, RealCache()).normalized(Context.Empty, RealCache()) -> StdLib.Nat.zero.normalized(Context.Empty, RealCache()),

      Bruinizer.bruinize(parse(
        "((lambda (Nat (Universe 0))\n   (lambda (n Nat) (WSup Nat true (lambda (u Unit) n))))\n (W (lambda (b Bool) ((Bool-ind Unit Empty) b))))"
      ))(Context.Empty, RealCache()).normalized(Context.Empty, RealCache()) -> StdLib.Nat.succ.normalized(Context.Empty, RealCache())


    )
  }
}
